package edu.uic.cs.cs582.process.impl;

import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;
import java.util.TreeSet;

import org.apache.log4j.Logger;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;

import edu.uic.cs.cs582.data.Component;
import edu.uic.cs.cs582.data.SynsetSet;
import edu.uic.cs.cs582.data.Synset;
import edu.uic.cs.cs582.data.Word;
import edu.uic.cs.cs582.misc.Config;
import edu.uic.cs.cs582.misc.LogHelper;
import edu.uic.cs.cs582.process.SatProcessor;
import edu.uic.cs.cs582.process.impl.SatIndexParser.WordIndex;
import edu.uic.cs.cs582.process.impl.SatIndexParser.Index;
import edu.uic.cs.cs582.process.impl.SatIndexParser.SynsetIndex;

public class CopyOfSatProcessorImpl implements SatProcessor
{
	private static final Logger LOGGER = LogHelper
			.getLogger(CopyOfSatProcessorImpl.class);

	private TreeSet<Integer> conflictSynsetIndexes = new TreeSet<Integer>();
	private TreeSet<Integer> conflictWordIndexes = new TreeSet<Integer>();

	private Component component = null;

	public CopyOfSatProcessorImpl(Component component)
	{
		this.component = component;
	}

	@Override
	public boolean processSat(int[][] cnfArrays) throws TimeoutException
	{
		ISolver solver = SolverFactory.newDefault();
		solver.newVar(Config.MAXVAR);
		solver.setTimeoutMs(Config.TIMEOUT);
		for (int[] clause : cnfArrays)
		{
			try
			{
				//				System.out.println(Arrays.toString(clause));
				solver.addClause(new VecInt(clause));
			}
			catch (ContradictionException e)
			{
				//				System.out.println(e.getMessage());
				if (LOGGER.isDebugEnabled())
				{
					LOGGER.debug("Catch ContradictionException. ");
				}

				//				int iii = ((WordIndex) SatIndexParser.parseIndex(11,
				//						component)).getWordIndexInOneComponent();
				//				System.out.println(component.getWordByIndex(iii));

				for (int i : clause)
				{
					Index index = SatIndexParser.parseIndex(i, component);
					if (index instanceof SynsetIndex)
					{
						conflictSynsetIndexes.add(((SynsetIndex) index)
								.getSynsetIndex());
						//						System.out.println("*************** synset: "
						//								+ i
						//								+ " "
						//								+ component
						//										.getSynsetByIndex(((SynsetIndex) index)
						//												.getSynsetIndex()));
					}
					else if (index instanceof WordIndex)
					{
						conflictWordIndexes.add(((WordIndex) index)
								.getWordIndexInOneComponent());
						//						System.out.println("*************** word: "
						//								+ i
						//								+ " "
						//								+ component
						//										.getWordByIndex(((WordIndex) index)
						//												.getWordIndexInOneComponent()));
					}
				}
			}
		}

		// if there's conflict happening when add variables into the solver,
		// return false, and there's no need for further checking
		if (!conflictSynsetIndexes.isEmpty() || !conflictWordIndexes.isEmpty())
		{
			return false;
		}
		/////////////////////

		solver.setSearchListener(new ConflictDetectingListener(
				conflictSynsetIndexes, conflictWordIndexes, component));

		LOGGER.debug("Begin to solve SAT. ");
		boolean result = solver.isSatisfiable();
		LOGGER.debug("End to solve SAT. Result is [" + result + "]. ");

		return result;
	}

	private Set<Synset> getConflictSynset()
	{
		HashSet<Synset> result = new HashSet<Synset>(
				conflictSynsetIndexes.size());
		for (Integer index : conflictSynsetIndexes)
		{
			result.add(component.getSynsetByIndex(index));
		}

		return result;
	}

	/*public Map<Synset, Set<Word>> getConflictWordsBySynset()
	{
		Map<Synset, Set<Word>> result = new HashMap<Synset, Set<Word>>();

		Set<Word> allWords = component.getAllWords();
		Set<Synset> allConflictSynsets = getConflictSynset();

		boolean hasChanged = false;
		do
		{
			hasChanged = false;

			for (Word word : allWords)
			{
				if (isWordContainsNonConflictMajoritySynset(word,
						allConflictSynsets))
				{
					continue;
				}

				if (!hasChanged
						&& allConflictSynsets.addAll(word
								.getAllSynsetsInMajoritySynsets()))
				{
					hasChanged = true;
				}

				for (Synset conflictingSynset : word
						.getAllSynsetsInMajoritySynsets())
				{
					//					if (isOneMajoritySynsetContainsGivenSynset(word,
					//							conflictingSynset))
					//					{
					Set<Word> wordList = result.get(conflictingSynset);
					if (wordList == null)
					{
						wordList = new TreeSet<Word>();
						result.put(conflictingSynset, wordList);
					}
					wordList.add(word);
					//					}
				}

			}
		}
		while (hasChanged);

		// post-process, remove all conflict list contain only one word
		Iterator<Entry<Synset, Set<Word>>> iterator = result.entrySet()
				.iterator();
		while (iterator.hasNext())
		{
			Set<Word> words = iterator.next().getValue();
			if (words.size() == 1)
			{
				iterator.remove();
			}
		}

		return result;
	}*/

	@Override
	public Map<Synset, Set<Word>> getConflictWordsBySynset()
	{
		Map<Synset, Set<Word>> result = new HashMap<Synset, Set<Word>>();

		Set<Word> allWords = component.getAllWords();
		Set<Synset> allConflictSynsets = getConflictSynset();
		if (allConflictSynsets.isEmpty())
		{
			return result;
		}

		for (Word word : allWords)
		{
			if (isWordContainsNonConflictMajoritySynset(word,
					allConflictSynsets))
			{
				continue;
			}

			// here, all majority-synsets contain some conflict synset
			// we need to get a map to tell which word has which synsets
			for (Synset conflictingSynset : allConflictSynsets)
			{
				if (doesAnyMajoritySynsetContainGivenSynset(word,
						conflictingSynset))
				{
					Set<Word> wordList = result.get(conflictingSynset);
					if (wordList == null)
					{
						wordList = new TreeSet<Word>();
						result.put(conflictingSynset, wordList);
					}
					wordList.add(word);
				}
			}
		}

		return result;
	}

	private boolean isWordContainsNonConflictMajoritySynset(Word word,
			Set<Synset> allConflictSynsets)
	{
		for (Set<Synset> eachMajority : word.getMajoritySynsets())
		{
			boolean isMajorityContainsConflict = false;
			for (Synset eachConflictSynset : allConflictSynsets)
			{
				if (eachMajority.contains(eachConflictSynset))
				{
					isMajorityContainsConflict = true;
					break;
				}
			}

			if (!isMajorityContainsConflict)
			{
				return true;
			}
		}

		return false;
	}

	public boolean doesAnyMajoritySynsetContainGivenSynset(Word word,
			Synset conflictingSynset)
	{
		for (SynsetSet eachMajoritySynsets : word.getMajoritySynsets())
		{
			if (eachMajoritySynsets.contains(conflictingSynset))
			{
				return true;
			}
		}

		return false;
	}

	@Override
	public Map<SynsetSet, Set<Word>> getConflictWordsBySynsetsInMajority()
	{
		Map<SynsetSet, Set<Word>> conflictingWordsByMajoritySynsets = initializeConflictingMajoritySynsets();

		//		boolean hasChanged = false;
		//		do
		//		{
		//			hasChanged = false;

		for (Word word : component.getAllWords())
		{
			Integer otherWordIndex = component.getIndexOfWord(word);
			if (conflictWordIndexes.contains(otherWordIndex))
			{
				// the conflicting words that have already processed in above steps
				continue;
			}

			// if one word has only one majority-synset, 
			// and the majority-synset has common with some known as inconsistent
			SynsetSet theOnlyMajoritySynsets = getTheOnlyOneMajoritySynsetsWhichIsInConflicting(
					word, conflictingWordsByMajoritySynsets);
			if (theOnlyMajoritySynsets != null)
			{
				conflictWordIndexes.add(otherWordIndex);
				Set<Word> conflictingWords = conflictingWordsByMajoritySynsets
						.get(theOnlyMajoritySynsets);
				if (conflictingWords == null)
				{
					conflictingWords = new TreeSet<Word>();
					conflictingWordsByMajoritySynsets.put(
							theOnlyMajoritySynsets, conflictingWords);
					//						hasChanged = true;
				}
				conflictingWords.add(word);

				continue;
			}

			// the words that haven't been reported, but may be the cause of conflict

			// if word doesn't have free majority-synsets
			// the word must be inconsistent
			if (!hasConflictFreeMajoritySynsets(word,
					conflictingWordsByMajoritySynsets))
			{
				conflictWordIndexes.add(otherWordIndex);

				for (SynsetSet majoritySynsetsOfWord : word
						.getMajoritySynsets())
				{
					Set<Word> conflictingWords = conflictingWordsByMajoritySynsets
							.get(majoritySynsetsOfWord);
					if (conflictingWords == null)
					{
						conflictingWords = new TreeSet<Word>();
						conflictingWordsByMajoritySynsets.put(
								majoritySynsetsOfWord, conflictingWords);
						//							hasChanged = true;
					}
					conflictingWords.add(word);
				}
			}
		}
		//		}
		//		while (hasChanged);

		return conflictingWordsByMajoritySynsets;
	}

	private SynsetSet getTheOnlyOneMajoritySynsetsWhichIsInConflicting(
			Word word,
			Map<SynsetSet, Set<Word>> conflictingWordsByMajoritySynsets)
	{
		for (Entry<SynsetSet, Set<Word>> knownConflicting : conflictingWordsByMajoritySynsets
				.entrySet())
		{
			SynsetSet conflictingMajoritySynsets = knownConflicting.getKey();
			List<SynsetSet> allMajoritySynsetsOfTheWord = word
					.getMajoritySynsets();
			if (allMajoritySynsetsOfTheWord.size() == 1
					&& allMajoritySynsetsOfTheWord.get(0).hasCommon(
							conflictingMajoritySynsets))
			{
				return allMajoritySynsetsOfTheWord.get(0);
			}
		}

		return null;
	}

	// if a word is said to be inconsistent, all its majority-synsets must be inconsistent, 
	// otherwise the certain polarity can be assigned to that 'conflict-free' majority-synsets 
	private Map<SynsetSet, Set<Word>> initializeConflictingMajoritySynsets()
	{
		Map<SynsetSet, Set<Word>> conflictingWordsByMajoritySynsets = new HashMap<SynsetSet, Set<Word>>();

		// for each conflicting word
		for (Integer wordIndex : conflictWordIndexes)
		{
			Word conflictingWord = component.getWordByIndex(wordIndex);
			List<SynsetSet> allMajoritySynsetsOfOneWord = conflictingWord
					.getMajoritySynsets();
			// all its majority-synsets are in conflicting
			for (SynsetSet majoritySynsets : allMajoritySynsetsOfOneWord)
			{
				Set<Word> conflictingWords = conflictingWordsByMajoritySynsets
						.get(majoritySynsets);
				if (conflictingWords == null)
				{
					conflictingWords = new TreeSet<Word>();
					conflictingWordsByMajoritySynsets.put(majoritySynsets,
							conflictingWords);
				}
				conflictingWords.add(conflictingWord);
			}
		}
		return conflictingWordsByMajoritySynsets;
	}

	private boolean hasConflictFreeMajoritySynsets(Word word,
			Map<SynsetSet, Set<Word>> allKnownConflictingMajoritySynsets)
	{
		for (SynsetSet majoritySynsetsOfWord : word.getMajoritySynsets())
		{
			boolean hasCommon = false;
			for (SynsetSet knownConflictingMajoritySynsets : allKnownConflictingMajoritySynsets
					.keySet())
			{
				// the polarities should not be the same one
				// has no common -> there is free
				if (majoritySynsetsOfWord
						.hasCommon(knownConflictingMajoritySynsets))
				{
					hasCommon = true;
					break;
				}
			}

			if (!hasCommon)
			{
				return true;
			}
		}

		return false;
	}
}
